import scala.util.parsing.combinator._

trait Binding {
  // represents a variable name
	type Name
	// creates a fresh name
	def Name(n: String): Name
	
	// something that contains Name's
	type HasBinder[T]
	
	// some construct of type T in which the Name n is bound
	type \\[T]
	def \\[T](n: Name, scope: HasBinder[T]): \\[T]
}

trait ContextualParsers extends Parsers with Binding {
  type Context <: ContextCore

  val Context: ContextCompanion
  trait ContextCompanion {
    val empty: Context = apply{name => None}
    def apply(f: String => Option[Name]): Context
  }
  
  trait ContextCore extends (String => Option[Name]) {
    def bind(nameParser: Parser[String]): Parser[(Context, Name)] 
      = (for(name <- nameParser) yield {
            val n=Name(name)
            (this(name) = n, n)
        })
        
    def bound(nameParser: Parser[String]): Parser[Name]  
      = (for(name   <- nameParser;
             binder <- lookup(name)) yield binder)
             
    def lookup(name: String): Parser[Name] = this(name) match {
      case None => failure explain("unbound name: "+name)
      case Some(b) => success(b)
    }
    
    def in[T](p: Context => Parser[HasBinder[T]]): Pair[Context, Name] => Parser[\\[T]] = {case (ctx, n) => p(ctx) ^^ (\\(n, _))}
    
    def update(rawName: String, binder: Name): Context = Context{name => if(name == rawName) Some(binder) else this(name) }
  }
}

trait Lexical extends Parsers {
  type Elem = Char
  import scala.util.parsing.input.CharArrayReader
  
  // these combinators do the lexical analysis, which we have not separated explicitly from the syntactical analysis
  def letter = acceptIf(_.isLetter) expected("letter")
  def digit = acceptIf(_.isDigit) expected("digit")
  def ws = rep1(accept(' ')) expected("whitespace")
  // hint: only wrap wss(...) around the parsers that really need it
  def wss[T](p: Parser[T]): Parser[T] = opt(ws) ~> p <~ opt(ws)
  def ident = rep1(letter, letter | digit) ^^ {_.mkString("")} expected("identifier")
  def eoi = accept(CharArrayReader.EofCh)
}

trait LambdaParser extends Syntax with Lexical with ContextualParsers {  
  // Context tracks which variables are bound, the generic functionality is implemented in ContextualParsers
  // Here, we only specify how to create our Context class
  object Context extends ContextCompanion {
    def apply(f: String => Option[Name]): Context = new Context { def apply(n: String) = f(n) }
  }
  
  // since parsing a term depends on the variable bindings we have previously added to the context,
  // we put these parsers in a Context, which provides the `bind`, `in`, and `bound` combinators
  // these combinators take care of variable binding
  trait Context extends ContextCore {
    def term = chainl1(termSingle, ws ^^^ (App(_: Term, _: Term)))
    def termSingle: Parser[Term] = 
      ( '(' ~> term <~ ')'
      | '\\' ~> bind(wss(ident)) >> in{ctx => '.' ~> wss(ctx.term)} ^^ Abs
      | bound(ident)                                      ^^ Var
      )
  }
 
  import scala.util.parsing.input.Reader
  def parse(input: Reader[Char]) = (wss(Context.empty.term) <~ eoi)(input)
}


trait DummyBinding extends Binding {
	class HasBinder[T]
	class Name
	def Name(n: String): Name = new Name
	class \\[T]
	def \\[T](n: Name, scope: HasBinder[T]): \\[T] = new \\[T]
}

trait Syntax extends DummyBinding {
  trait Term extends HasBinder[Term]
  case class Var(name: Name) extends Term
  case class Abs(abs: \\[Term]) extends Term 
  case class App(fun: Term, arg: Term) extends Term
}


/*object ParsingTest extends LambdaParser {
  def main(args: Array[String]) = println(parse(args(0)))
}*/